The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^3)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

a(l(x1)) → l(a(x1))
r(a(a(x1))) → a(a(r(x1)))
b(l(x1)) → b(a(r(x1)))
r(b(x1)) → l(b(x1))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(l(z0)) → l(a(z0))
r(a(a(z0))) → a(a(r(z0)))
r(b(z0)) → l(b(z0))
b(l(z0)) → b(a(r(z0)))

Tuples:

A(l(z0)) → c(A(z0))
R(a(a(z0))) → c1(A(a(r(z0))), A(r(z0)), R(z0))
R(b(z0)) → c2(B(z0))
B(l(z0)) → c3(B(a(r(z0))), A(r(z0)), R(z0))

S tuples:

A(l(z0)) → c(A(z0))
R(a(a(z0))) → c1(A(a(r(z0))), A(r(z0)), R(z0))
R(b(z0)) → c2(B(z0))
B(l(z0)) → c3(B(a(r(z0))), A(r(z0)), R(z0))

K tuples:none
Defined Rule Symbols:

a, r, b

Defined Pair Symbols:

A, R, B

Compound Symbols:

c, c1, c2, c3

(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace R(a(a(z0))) → c1(A(a(r(z0))), A(r(z0)), R(z0)) by

R(a(a(a(a(z0))))) → c1(A(a(a(a(r(z0))))), A(r(a(a(z0)))), R(a(a(z0))))
R(a(a(b(z0)))) → c1(A(a(l(b(z0)))), A(r(b(z0))), R(b(z0)))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(l(z0)) → l(a(z0))
r(a(a(z0))) → a(a(r(z0)))
r(b(z0)) → l(b(z0))
b(l(z0)) → b(a(r(z0)))

Tuples:

A(l(z0)) → c(A(z0))
R(b(z0)) → c2(B(z0))
B(l(z0)) → c3(B(a(r(z0))), A(r(z0)), R(z0))
R(a(a(a(a(z0))))) → c1(A(a(a(a(r(z0))))), A(r(a(a(z0)))), R(a(a(z0))))
R(a(a(b(z0)))) → c1(A(a(l(b(z0)))), A(r(b(z0))), R(b(z0)))

S tuples:

A(l(z0)) → c(A(z0))
R(b(z0)) → c2(B(z0))
B(l(z0)) → c3(B(a(r(z0))), A(r(z0)), R(z0))
R(a(a(a(a(z0))))) → c1(A(a(a(a(r(z0))))), A(r(a(a(z0)))), R(a(a(z0))))
R(a(a(b(z0)))) → c1(A(a(l(b(z0)))), A(r(b(z0))), R(b(z0)))

K tuples:none
Defined Rule Symbols:

a, r, b

Defined Pair Symbols:

A, R, B

Compound Symbols:

c, c2, c3, c1

(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace B(l(z0)) → c3(B(a(r(z0))), A(r(z0)), R(z0)) by

B(l(a(a(z0)))) → c3(B(a(a(a(r(z0))))), A(r(a(a(z0)))), R(a(a(z0))))
B(l(b(z0))) → c3(B(a(l(b(z0)))), A(r(b(z0))), R(b(z0)))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(l(z0)) → l(a(z0))
r(a(a(z0))) → a(a(r(z0)))
r(b(z0)) → l(b(z0))
b(l(z0)) → b(a(r(z0)))

Tuples:

A(l(z0)) → c(A(z0))
R(b(z0)) → c2(B(z0))
R(a(a(a(a(z0))))) → c1(A(a(a(a(r(z0))))), A(r(a(a(z0)))), R(a(a(z0))))
R(a(a(b(z0)))) → c1(A(a(l(b(z0)))), A(r(b(z0))), R(b(z0)))
B(l(a(a(z0)))) → c3(B(a(a(a(r(z0))))), A(r(a(a(z0)))), R(a(a(z0))))
B(l(b(z0))) → c3(B(a(l(b(z0)))), A(r(b(z0))), R(b(z0)))

S tuples:

A(l(z0)) → c(A(z0))
R(b(z0)) → c2(B(z0))
R(a(a(a(a(z0))))) → c1(A(a(a(a(r(z0))))), A(r(a(a(z0)))), R(a(a(z0))))
R(a(a(b(z0)))) → c1(A(a(l(b(z0)))), A(r(b(z0))), R(b(z0)))
B(l(a(a(z0)))) → c3(B(a(a(a(r(z0))))), A(r(a(a(z0)))), R(a(a(z0))))
B(l(b(z0))) → c3(B(a(l(b(z0)))), A(r(b(z0))), R(b(z0)))

K tuples:none
Defined Rule Symbols:

a, r, b

Defined Pair Symbols:

A, R, B

Compound Symbols:

c, c2, c1, c3

(7) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

R(b(z0)) → c2(B(z0))
R(a(a(a(a(z0))))) → c1(A(a(a(a(r(z0))))), A(r(a(a(z0)))), R(a(a(z0))))
R(a(a(b(z0)))) → c1(A(a(l(b(z0)))), A(r(b(z0))), R(b(z0)))
B(l(a(a(z0)))) → c3(B(a(a(a(r(z0))))), A(r(a(a(z0)))), R(a(a(z0))))
B(l(b(z0))) → c3(B(a(l(b(z0)))), A(r(b(z0))), R(b(z0)))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(l(z0)) → l(a(z0))
r(a(a(z0))) → a(a(r(z0)))
r(b(z0)) → l(b(z0))
b(l(z0)) → b(a(r(z0)))

Tuples:

A(l(z0)) → c(A(z0))

S tuples:

A(l(z0)) → c(A(z0))

K tuples:none
Defined Rule Symbols:

a, r, b

Defined Pair Symbols:

A

Compound Symbols:

c

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

A(l(z0)) → c(A(z0))

We considered the (Usable) Rules:none
And the Tuples:

A(l(z0)) → c(A(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(A(x₁)) = x₁ + x₁²   
POL(c(x₁)) = x₁   
POL(l(x₁)) = [1] + x₁   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(l(z0)) → l(a(z0))
r(a(a(z0))) → a(a(r(z0)))
r(b(z0)) → l(b(z0))
b(l(z0)) → b(a(r(z0)))

Tuples:

A(l(z0)) → c(A(z0))

S tuples:none
K tuples:

A(l(z0)) → c(A(z0))

Defined Rule Symbols:

a, r, b

Defined Pair Symbols:

A

Compound Symbols:

c

(11) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(12) BOUNDS(O(1), O(1))